(declare-fun a () Real)
(declare-fun b () Real)
(push)
(assert (= b 0))
(check-sat)
(assert (< (+ b 1) 0))
(push)
(assert (= (+ a b b) 0))
(push)
(check-sat)
